Web Page of CafeOBJ Specifications and Proof Scores for
ABP (Alternating Bit Protocol) and
QLOCK (Mutual Exclusion by Locking with Queue)
by Kokichi Futatsugi (JAIST)

abp-all-ps.cafe
abp-constLitl.cafe
abp-factTbu-ps.cafe
abp-factTbu.cafe
abp-genCheck.cafe
abp-genSt.cafe
abp-inv-1-ps.cafe
abp-inv-2-ps.cafe
abp-inv-3-ps-sht.cafe
abp-inv-3-ps.cafe
abp-prop.cafe
abp-sys.cafe
exState.cafe
genCases.cafe
genCheck.cafe
pnat.cafe
predCj.cafe
qlock-all-ps.cafe
qlock-constAndLitl.cafe
qlock-factTbu.cafe
qlock-genCheck.cafe
qlock-genStTerm.cafe
qlock-inv-1-ps.cafe
qlock-inv-2-ps.cafe
qlock-inv-3-ps.cafe
qlock-natQuSet.cafe
qlock-pq-1-ps.cafe
qlock-pq-2-ps.cafe
qlock-pq-3-ps.cafe
qlock-pq-4-ps.cafe
qlock-prop.cafe
qlock-sys-ex.cafe
qlock-sys.cafe


zip file for the directory containing all the above files


The five files exState.cafe, exState.cafe, genCases.cafe, genCheck.cafe, pnat.cafe, and predCj.cafe contain the generic proof scores. The files with the suffix "abp-" and "qlock-" contain the specifications and proof scores specific to ABP and QLOCK respectively.

Entering "input abp-all-ps.cafe" and "input qlock-all-ps.cafe" to the CafeOBJ system makes all proof scores for ABP and QLOCK be executed respectively. Be sure to execute the "full reset" command to initialize the CafeOBJ system between the two "input" commands.